Inference at * 1 0 4 1 3 
Iof proof for Lemma eq int cases test:

.....wf..... NILNIL

1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. P(if (i = j) then x else y fi )
8.   Type
9. (i = j)  
10. bb:. ((i = j) = bb)  Type
11. bb : 
  ((i = j) = bb)  Type 

latex

 by ((MemCD) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

x:A. B(x), , (i = j), if b then t else f fi , f(a), , , x:AB(x), Type, s = t, t  T